Nuprl Definition : R-ds 11,40

R-ds(Ri)
== es_realizer_ind(R;
== es_realizer_ind(fpf-empty;
== es_realizer_ind(left,right,rec1,rec2.fpf-join(id-deq; rec1rec2);
== es_realizer_ind(loc,T,x,v.if eq_id(loci) then fpf-single(xT) else fpf-empty fi ;
== es_realizer_ind(loc,T,x,L.if eq_id(loci) then fpf-single(xT) else fpf-empty fi ;
== es_realizer_ind(lnk,tag,L.fpf-empty;
== es_realizer_ind(loc,ds,knd,T,x,f.if eq_id(loci) then ds else fpf-empty fi ;
== es_realizer_ind(ds,knd,T,l,dt,g.if eq_id(source(l); i) then ds else fpf-empty fi ;
== es_realizer_ind(loc,ds,a,T,P.if eq_id(loci) then ds else fpf-empty fi ;
== es_realizer_ind(loc,k,L.fpf-empty;
== es_realizer_ind(loc,k,L.fpf-empty;
== es_realizer_ind(loc,x,L.fpf-empty) 
latex


Definitionsfpf-join(eqfg), id-deq, fpf-single(xv), source(l), if b then t else f fi , eq_id(ab), fpf-empty
FDL editor aliasesR-ds

origin